perm filename PFIB[AP,JRA] blob
sn#077776 filedate 1975-01-16 generic text, type T, neo UTF8
(CSYM AV00)
(THVSETQ (THV ANS) (LIST (LIST (QUOTE THV) (GENSYM))))
(THVSET (CAR (THV ANS)) NIL)
(THVSETQ (THV WF) NIL)
(THVSETQ (THV GCTR) 0)
(THVSETQ (THV ULS) T)
(THVSETQ (THV UF) NIL)
(THVSETQ (THV XN) 0)
(THVSETQ (THV ZN) 0)
(THVSETQ (THV YN) 0)
(THVSETQ (THV COMMENTLIST) NIL)
(THVSETQ (THV PLANL) NIL)
(THVSETQ (THV ASSL) NIL)
(THVSETQ (THV PASSUM) NIL)
(SETQ GTEMP NIL)
(SETQ CT NIL)
(SETQ BTSW NIL)
(THVSETQ (THV DG) NIL)
(SETQ AL NIL)
(SETQ AN 0)
(SETQ SRULES (QUOTE (((SUB1 (ADD1 X)) X) ((ADD1 (SUB1 X)) X))))
(SETQ SSW NIL)
(SETQ FIFOL NIL)
(SETQ LIFOL NIL)
(SETQ SN 0)
(SETQ PN 0)
(SETQ READY NIL)
(SETQ UNCERTLIST NIL)
(THVSETQ (THV DBLITS) NIL)
(THVSETQ (THV ASSERTLITS) NIL)
(THVSETQ (THV WASSERTLITS) NIL)
(SETQ JOINCOND NIL)
(THVSETQ (THV PROCLIST) NIL)
(THVSETQ (THV PROCDATA) NIL)
(THASSERT (ISVAR X3))
(THASSERT (INTEGER N))
(THASSERT (VFIB (2) (ADD1 (1)) R))
(THASSERT (VFIB (SUB1 (2)) (1) R))
(THVSETQ (THV FIBARGS) NIL)
(THVSETQ (THV FIBINST) NIL)
(DEFPROP FIBGREMLIN (THERASING (V1 V2) (FIB (THV V1) (THV V2) R) (THCOND ((MEMBER (THV FIBINST) (THV FIBARGS)) (~
THASSERT (WRONG PATH))))) THEOREM)
(THASSERT FIBGREMLIN)
(THVSETQ (THV NFIBARGS) NIL)
(THVSETQ (THV NFIBINST) NIL)
(DEFPROP NFIBGREMLIN (THERASING (V1 V2) (NFIB (THV V1) (THV V2) R) (THCOND ((MEMBER (THV NFIBINST) (THV NFIBARGS~
)) (THASSERT (WRONG PATH))))) THEOREM)
(THASSERT NFIBGREMLIN)
(THVSETQ (THV CARGS) NIL)
(THVSETQ (THV CINST) NIL)
(DEFPROP CGREMLIN (THERASING (V1 V2) (C (THV V1) (THV V2) R) (THCOND ((MEMBER (THV CINST) (THV CARGS)) (THASSERT~
(WRONG PATH))))) THEOREM)
(THASSERT CGREMLIN)
(THVSETQ (THV NCARGS) NIL)
(THVSETQ (THV NCINST) NIL)
(DEFPROP NCGREMLIN (THERASING (V1 V2) (NC (THV V1) (THV V2) R) (THCOND ((MEMBER (THV NCINST) (THV NCARGS)) (THAS~
SERT (WRONG PATH))))) THEOREM)
(THASSERT NCGREMLIN)
(THVSETQ (THV =ARGS) NIL)
(THVSETQ (THV =INST) NIL)
(DEFPROP =GREMLIN (THERASING (V1 V2) (= (THV V1) (THV V2) R) (THCOND ((MEMBER (THV =INST) (THV =ARGS)) (THASSERT~
(WRONG PATH))))) THEOREM)
(THASSERT =GREMLIN)
(THVSETQ (THV N=ARGS) NIL)
(THVSETQ (THV N=INST) NIL)
(DEFPROP N=GREMLIN (THERASING (V1 V2) (N= (THV V1) (THV V2) R) (THCOND ((MEMBER (THV N=INST) (THV N=ARGS)) (THAS~
SERT (WRONG PATH))))) THEOREM)
(THASSERT N=GREMLIN)
(THVSETQ (THV VFIBARGS) NIL)
(THVSETQ (THV VFIBINST) NIL)
(DEFPROP VFIBGREMLIN (THERASING (V1 V2) (VFIB (THV V1) (THV V2) R) (THCOND ((MEMBER (THV VFIBINST) (THV VFIBARGS~
)) (THASSERT (WRONG PATH))))) THEOREM)
(THASSERT VFIBGREMLIN)
(THVSETQ (THV NVFIBARGS) NIL)
(THVSETQ (THV NVFIBINST) NIL)
(DEFPROP NVFIBGREMLIN (THERASING (V1 V2) (NVFIB (THV V1) (THV V2) R) (THCOND ((MEMBER (THV NVFIBINST) (THV NVFIB~
ARGS)) (THASSERT (WRONG PATH))))) THEOREM)
(THASSERT NVFIBGREMLIN)
(SETQ RTTAFIB NIL)
(SETQ RFTAFIB NIL)
(DEFPROP TAFIB
(THCONSE (CGL V16 V15 V14 V13 (LSTTAFIB (QUOTE (V14 V13))))
(VFIB (THV V13) (THV V14) R)
(THSETQ (THV LCTR) (THV GCTR))
(SETQ THME (ADD1 THME))
(TREEPATH TAFIB (VFIB (THV V13) (THV V14) R))
(TRACEINFO1)
(THOR T (TRACEINFO2 TAFIB))
(COND ((TTYIN) (ADVICESYS)) (T T))
(THGOAL (VFIB (THEV (LIST (QUOTE SUB1) (THV V13))) (THV V15) R) (THTBF FILTEROP))
(THGOAL (VFIB (THEV (LIST (QUOTE SUB1) (LIST (QUOTE SUB1) (THV V13)))) (THV V16) R)
(THTBF FILTEROP))
(THCOND ((THASVAL (THV V14)) (EQUAL (THV V14) (LIST (QUOTE PLUS) (THV V15) (THV V16))))
(T (THSETQ (THV V14) (LIST (QUOTE PLUS) (THV V15) (THV V16)))))
(THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
(SETQ THMS (ADD1 THMS))
(COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
THEOREM)
(SETQ RTTFIB NIL)
(SETQ RFTFIB NIL)
(DEFPROP TFIB
(THCONSE (V10 V9 V5 V3 V8 V2 V1 FT NT CGL LCTR LWF LUF PS PB BP SASSERTLITS INVAR1 INVAR2 CTST)
(FIB (THV V3) (THV V8) R)
(THSETQ (THV LCTR) (THV GCTR))
(SETQ THME (ADD1 THME))
(TREEPATH TFIB (FIB (THV V3) (THV V8) R))
(TRACEINFO1)
(THOR T (TRACEINFO2 TFIB))
(COND ((TTYIN) (ADVICESYS)) (T T))
(THSETQ (THV LWF) NIL T T)
(THCOND ((NOT (THV WF)) (THSETQ (THV LWF) T)) (T T))
(THSETQ (THV WF) T)
(THSETQ (THV LUF) NIL T T)
(THSETQ (THV PS) (EVAL (CAR (THV ANS))) T T)
(THSET (CAR (THV ANS)) NIL)
(THGOAL (INTEGER (THV V8)))
(NEWVAR (THV V1) (THV V2))
(THGOAL (C (THV V1) (2) R) (THTBF FILTEROP))
(THCOND ((THAND (THASVAL (THV V1)))
(THSETQ (THV CARGS) (CONS (LIST (THV V1) (QUOTE (2))) (THV CARGS))))
(T T))
(THGOAL (C (THV V2) (1) R) (THTBF FILTEROP))
(THCOND ((THAND (THASVAL (THV V2)))
(THSETQ (THV CARGS) (CONS (LIST (THV V2) (QUOTE (1))) (THV CARGS))))
(T T))
(THGOAL (C (THV V3) (THEV (LIST (QUOTE ADD1) (LIST (QUOTE 1)))) R) (THTBF FILTEROP))
(THCOND ((THAND (THASVAL (THV V3)))
(THSETQ (THV CARGS)
(CONS (LIST (THV V3) (LIST (QUOTE ADD1) (LIST (QUOTE 1)))) (THV CARGS))))
(T T))
(THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
(THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
(THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
(THSETQ (THV BP) (EVAL (CAR (THV ANS))) T T)
(THSET (CAR (THV ANS)) NIL)
(THOR T (THFAIL THEOREM))
REP
(THGOAL (C (THV V1) (THV V5) R) (THTBF FILTERAX))
(THGOAL (C (THV V2) (THV V9) R) (THTBF FILTERAX))
(THGOAL (C (THV V3) (THV V10) R) (THTBF FILTERAX))
(THGOAL (VFIB (THV V5) (THV V10) R) (THTBF FILTERAX))
(THGOAL (VFIB (THEV (LIST (QUOTE SUB1) (THV V5))) (THV V9) R) (THTBF FILTERAX))
(THSETQ (THV INVAR1)
(LIST (SIMPLE (LIST (QUOTE VFIB) (LIST (QUOTE SUB1) (THV V5)) (THV V9) (QUOTE R)))
(SIMPLE (LIST (QUOTE VFIB) (THV V5) (THV V10) (QUOTE R)))
(SIMPLE (LIST (QUOTE C) (THV V3) (THV V10) (QUOTE R)))
(SIMPLE (LIST (QUOTE C) (THV V2) (THV V9) (QUOTE R)))
(SIMPLE (LIST (QUOTE C) (THV V1) (THV V5) (QUOTE R))))
T
T)
(THSETQ (THV CTST) (LIST (QUOTE >) (THV V5) (THV V8)))
(THOR T (THFAIL THEOREM))
(THSETQ (THV SASSERTLITS) (THV ASSERTLITS) T T)
(THGOAL (C (THV V1) (THEV (LIST (QUOTE ADD1) (THV V5))) R) (THTBF FILTEROP))
(THCOND ((THAND (THASVAL (THV V1)))
(THSETQ (THV CARGS)
(CONS (LIST (THV V1) (LIST (QUOTE ADD1) (THV V5))) (THV CARGS))))
(T T))
(THGOAL (FIB (THV V2) (THV V5) R) (THTBF FILTEROP))
(THCOND ((THAND (THASVAL (THV V5)) (THASVAL (THV V2)))
(THSETQ (THV FIBARGS) (CONS (LIST (THV V2) (THV V5)) (THV FIBARGS))))
(T T))
(THGOAL (FIB (THV V3) (THEV (LIST (QUOTE ADD1) (THV V5))) R) (THTBF FILTEROP))
(THCOND ((THAND (THASVAL (THV V3)))
(THSETQ (THV FIBARGS)
(CONS (LIST (THV V3) (LIST (QUOTE ADD1) (THV V5))) (THV FIBARGS))))
(T T))
(THCOND ((NULL (THV FIBARGS)) T) (T (THSETQ (THV FIBARGS) (CDR (THV FIBARGS)) T T)))
(THCOND ((NULL (THV FIBARGS)) T) (T (THSETQ (THV FIBARGS) (CDR (THV FIBARGS)) T T)))
(THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
(THSETQ (THV V10) (QUOTE THUNASSIGNED))
(THSETQ (THV V9) (QUOTE THUNASSIGNED))
(THSETQ (THV V5) (QUOTE THUNASSIGNED))
(THGOAL (C (THV V1) (THV V5) R) (THTBF FILTERAX))
(THGOAL (C (THV V2) (THV V9) R) (THTBF FILTERAX))
(THGOAL (C (THV V3) (THV V10) R) (THTBF FILTERAX))
(THGOAL (VFIB (THV V5) (THV V10) R) (THTBF FILTERAX))
(THGOAL (VFIB (THEV (LIST (QUOTE SUB1) (THV V5))) (THV V9) R) (THTBF FILTERAX))
(THCOND ((NOT (THASVAL (THV V10))) (THSETQ (THV V10) (QUOTE ##))) (T T))
(THCOND ((NOT (THASVAL (THV V9))) (THSETQ (THV V9) (QUOTE ##))) (T T))
(THCOND ((NOT (THASVAL (THV V5))) (THSETQ (THV V5) (QUOTE ##))) (T T))
(THSETQ (THV PB) (EVAL (CAR (THV ANS))) T T)
(THSETQ (THV INVAR2)
(LIST (SIMPLE (LIST (QUOTE VFIB) (LIST (QUOTE SUB1) (THV V5)) (THV V9) (QUOTE R)))
(SIMPLE (LIST (QUOTE VFIB) (THV V5) (THV V10) (QUOTE R)))
(SIMPLE (LIST (QUOTE C) (THV V3) (THV V10) (QUOTE R)))
(SIMPLE (LIST (QUOTE C) (THV V2) (THV V9) (QUOTE R)))
(SIMPLE (LIST (QUOTE C) (THV V1) (THV V5) (QUOTE R))))
T
T)
(THCOND ((THASVAL (THV FT))
(THSETQ (THV NT)
(COMPCHANGES (THV INVAR1)
(THV INVAR2)
(INCRELIT (THV SASSERTLITS) (REVERSE (THV ASSERTLITS))))))
(T
(THSETQ (THV FT)
(COMPCHANGES (THV INVAR1)
(THV INVAR2)
(INCRELIT (THV SASSERTLITS) (REVERSE (THV ASSERTLITS)))))))
(THCOND ((AND (NOT (THASVAL (THV NT))) (AMBIG (THV FT))) (THSETQ (THV V10)
(QUOTE THUNASSIGNED))
(THSETQ (THV V9)
(QUOTE THUNASSIGNED))
(THSETQ (THV V5)
(QUOTE THUNASSIGNED))
(THSET (CAR (THV ANS)) NIL)
(THGO REP))
(T T))
(SETQ GTEMP
(WHILASSEM (THV BP)
(THV PB)
(COND ((THASVAL (THV NT)) (THV NT)) (T (THV FT)))
(THV CTST)))
(THSETQ (THV PB) GTEMP T T)
(THSET (CAR (THV ANS)) (APPEND (THV PB) (THV PS)))
(THASSERT (FIB (THV V3) (THV V8) R))
(THCOND ((THV ULS)
(THSETQ (THV ASSERTLITS)
(CONS (LIST (LIST (QUOTE FIB) (THV V3) (THV V8) (QUOTE R))
(LIST (QUOTE A) (QUOTE A)))
(THV ASSERTLITS))))
(T
(THSETQ (THV WASSERTLITS)
(CONS (LIST (LIST (QUOTE FIB) (THV V3) (THV V8) (QUOTE R))
(LIST (QUOTE A) (QUOTE A)))
(THV WASSERTLITS)))))
(SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
(THCOND ((THV LWF) (THSETQ (THV WF) NIL T T)
(THSETQ (THV BT) NIL T T)
(SETQ GANS (REMBT GANS)))
(T T))
(THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
(THCOND ((THV LUF) (THSETQ (THV UF) NIL T T) (THSETQ (THV ULS) T)) (T T))
(THCOND ((THV ULS)
(THSETQ (THV ASSERTLITS)
(CONS (LIST (LIST (QUOTE FIB) (THV V3) (THV V8) (QUOTE R))
(LIST (QUOTE A) (QUOTE A)))
(THV ASSERTLITS))))
(T
(THSETQ (THV WASSERTLITS)
(CONS (LIST (LIST (QUOTE FIB) (THV V3) (THV V8) (QUOTE R))
(LIST (QUOTE A) (QUOTE A)))
(THV WASSERTLITS)))))
(COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
THEOREM)
(SETQ RTTDFIB NIL)
(SETQ RFTDFIB NIL)
(DEFPROP TDFIB
(THCONSE (CGL V3 V2 V4 (LSTTDFIB (QUOTE (V2 V4))))
(FIB (THV V4) (THV V2) R)
(THSETQ (THV LCTR) (THV GCTR))
(SETQ THME (ADD1 THME))
(THUNIQUE LSTTDFIB)
(TREEPATH TDFIB (FIB (THV V4) (THV V2) R))
(TRACEINFO1)
(THOR T (TRACEINFO2 TDFIB))
(COND ((TTYIN) (ADVICESYS)) (T T))
(THGOAL (VFIB (THV V2) (THV V3) R) (THTBF FILTEROP))
(THCOND ((THAND (THASVAL (THV V3)) (THASVAL (THV V2)))
(THSETQ (THV VFIBARGS) (CONS (LIST (THV V2) (THV V3)) (THV VFIBARGS))))
(T T))
(THGOAL (C (THV V4) (THV V3) R) (THTBF FILTEROP))
(THCOND ((THAND (THASVAL (THV V3)) (THASVAL (THV V4)))
(THSETQ (THV CARGS) (CONS (LIST (THV V4) (THV V3)) (THV CARGS))))
(T T))
(THCOND ((NULL (THV CARGS)) T) (T (THSETQ (THV CARGS) (CDR (THV CARGS)) T T)))
(THCOND ((NULL (THV VFIBARGS)) T) (T (THSETQ (THV VFIBARGS) (CDR (THV VFIBARGS)) T T)))
(THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
(SETQ THMS (ADD1 THMS))
(COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
THEOREM)
(SETQ RT← NIL)
(SETQ RF← NIL)
(DEFPROP ←
(THCONSE (CGL A1 V1 D1 (LST← (QUOTE (A1 V1))))
(C (THV V1) (THV A1) R)
(THSETQ (THV LCTR) (THV GCTR))
(SETQ THME (ADD1 THME))
(THUNIQUE LST←)
(TREEPATH ← (C (THV V1) (THV A1) R))
(TRACEINFO1)
(THOR T (TRACEINFO2 ←))
(COND ((TTYIN) (ADVICESYS)) (T T))
(THGOAL (ISVAR (THV V1)))
(THCOND ((THGOAL (C (THV V1) (THV D1) R)) (THSETQ (THV CINST) (LIST (THV V1) (THV D1))))
(T T))
(THCOND ((THGOAL (C (THV V1) (THV D1) R)) (THERASE (C (THV V1) (THV D1) R) (THTBF THTRUE)))
(T T))
(THCOND ((THERASE (WRONG PATH)) (THFAIL THEOREM)) (T T))
(THSET (CAR (THV ANS))
(CONS (CONS (QUOTE ←) (LIST (THV V1) (THV A1))) (EVAL (CAR (THV ANS)))))
(THSETQ (THV DBLITS) (CONS (CDAR CT) (THV DBLITS)))
(SETQ THMS (ADD1 THMS))
(THASSERT (C (THV V1) (THV A1) R))
(THCOND ((THV ULS)
(THSETQ (THV ASSERTLITS)
(CONS (LIST (LIST (QUOTE C) (THV V1) (THV A1) (QUOTE R))
(LIST (QUOTE A) (QUOTE A)))
(THV ASSERTLITS))))
(T
(THSETQ (THV WASSERTLITS)
(CONS (LIST (LIST (QUOTE C) (THV V1) (THV A1) (QUOTE R))
(LIST (QUOTE A) (QUOTE A)))
(THV WASSERTLITS)))))
(PRINT (REVERSE (EVAL (CAR (THV ANS)))))
(SETQ GANS (REVERSE (EVAL (CAR (THV ANS)))))
(COND ((*GREAT (LENGTH GANS) (LENGTH LGANS)) (SETQ LGANS GANS)) (T T))
(THDO (TERPRI))
(COND ((EQ (QUOTE IF) (CADAR CT)) (ELSECLAUSE)) (T (THSETQ CT (CDR CT) T T))))
THEOREM)
(THASSERT ←)
(THASSERT TDFIB)
(THASSERT TFIB)
(THASSERT TAFIB)
(DEFPROP RESTOREPROP
(LAMBDA NIL
(PROG NIL
(SETQ STAT T)
(SETQ FUNDEFLIST
(QUOTE
((ADD1 (X) (/( X /+ 1 /))) (SUB1 (X) (/( X /- 1 /))) (PLUS (X Y) (/( X /+ Y /))))))
(PUTPROP (QUOTE CFIB) T (QUOTE DEF))
(PUTPROP (QUOTE CFIB) (QUOTE NIL) (QUOTE UNIQ))
(PUTPROP (QUOTE CFIB) (QUOTE NIL) (QUOTE UNCERT))
(PUTPROP (QUOTE CFIB) (QUOTE NIL) (QUOTE PARTIAL))
(PUTPROP (QUOTE CFIB) (QUOTE T) (QUOTE FLUENT))
(PUTPROP (QUOTE VFIB) T (QUOTE DEF))
(PUTPROP (QUOTE VFIB) (QUOTE NIL) (QUOTE UNIQ))
(PUTPROP (QUOTE VFIB) (QUOTE NIL) (QUOTE UNCERT))
(PUTPROP (QUOTE VFIB) (QUOTE NIL) (QUOTE PARTIAL))
(PUTPROP (QUOTE VFIB) (QUOTE T) (QUOTE FLUENT))
(PUTPROP (QUOTE =) T (QUOTE DEF))
(PUTPROP (QUOTE =) (QUOTE NIL) (QUOTE UNIQ))
(PUTPROP (QUOTE =) (QUOTE NIL) (QUOTE UNCERT))
(PUTPROP (QUOTE =) (QUOTE NIL) (QUOTE PARTIAL))
(PUTPROP (QUOTE =) (QUOTE T) (QUOTE FLUENT))
(PUTPROP (QUOTE INTEGER) T (QUOTE DEF))
(PUTPROP (QUOTE INTEGER) (QUOTE NIL) (QUOTE UNIQ))
(PUTPROP (QUOTE INTEGER) (QUOTE NIL) (QUOTE UNCERT))
(PUTPROP (QUOTE INTEGER) (QUOTE NIL) (QUOTE PARTIAL))
(PUTPROP (QUOTE INTEGER) (QUOTE NIL) (QUOTE FLUENT))
(PUTPROP (QUOTE >) T (QUOTE DEF))
(PUTPROP (QUOTE >) (QUOTE NIL) (QUOTE UNIQ))
(PUTPROP (QUOTE >) (QUOTE NIL) (QUOTE UNCERT))
(PUTPROP (QUOTE >) (QUOTE NIL) (QUOTE PARTIAL))
(PUTPROP (QUOTE >) (QUOTE NIL) (QUOTE FLUENT))
(PUTPROP (QUOTE FIB) T (QUOTE DEF))
(PUTPROP (QUOTE FIB) (QUOTE NIL) (QUOTE UNIQ))
(PUTPROP (QUOTE FIB) (QUOTE NIL) (QUOTE UNCERT))
(PUTPROP (QUOTE FIB) (QUOTE NIL) (QUOTE PARTIAL))
(PUTPROP (QUOTE FIB) (QUOTE T) (QUOTE FLUENT))
(PUTPROP (QUOTE C) T (QUOTE DEF))
(PUTPROP (QUOTE C) (QUOTE (X *)) (QUOTE UNIQ))
(PUTPROP (QUOTE C) (QUOTE NIL) (QUOTE UNCERT))
(PUTPROP (QUOTE C) (QUOTE NIL) (QUOTE PARTIAL))
(PUTPROP (QUOTE C) (QUOTE T) (QUOTE FLUENT))
(PUTPROP (QUOTE TAFIB) (QUOTE NIL) (QUOTE INEQ))
(PUTPROP (QUOTE TAFIB) (QUOTE T) (QUOTE REC))
(PUTPROP (QUOTE TAFIB) (QUOTE NIL) (QUOTE ASSUM))
(PUTPROP (QUOTE TAFIB) (QUOTE NIL) (QUOTE ARG))
(PUTPROP (QUOTE TAFIB) T (QUOTE AX))
(PUTPROP (QUOTE TDFIB) (QUOTE NIL) (QUOTE INEQ))
(PUTPROP (QUOTE TDFIB) (QUOTE NIL) (QUOTE REC))
(PUTPROP (QUOTE TDFIB) (QUOTE NIL) (QUOTE ASSUM))
(PUTPROP (QUOTE TDFIB) (QUOTE NIL) (QUOTE ARG))
(PUTPROP (QUOTE TDFIB) T (QUOTE DEF))
(PUTPROP (QUOTE TFIB) (QUOTE NIL) (QUOTE INEQ))
(PUTPROP (QUOTE TFIB) (QUOTE NIL) (QUOTE REC))
(PUTPROP (QUOTE TFIB) (QUOTE NIL) (QUOTE ASSUM))
(PUTPROP (QUOTE TFIB) (QUOTE NIL) (QUOTE ARG))
(PUTPROP (QUOTE TFIB) T (QUOTE ITER))
(PUTPROP (QUOTE ←) (QUOTE NIL) (QUOTE INEQ))
(PUTPROP (QUOTE ←) (QUOTE NIL) (QUOTE REC))
(PUTPROP (QUOTE ←) (QUOTE NIL) (QUOTE ASSUM))
(PUTPROP (QUOTE ←) (QUOTE (V1 A1)) (QUOTE ARG))
(PUTPROP (QUOTE ←) T (QUOTE OP))))
EXPR)